rust verification tools
2022-01-13 ยท 1 min read
Rudra #
Github: https://github.com/sslab-gatech/Rudra
Rudra is a static analyzer to detect common undefined behaviors in Rust programs. It is capable of analyzing single Rust packages as well as all the packages on crates.io.
Prusti #
Github: https://github.com/viperproject/prusti-dev
Prusti is a prototype verifier for Rust, built upon the Viper verification infrastructure.
By default Prusti verifies absence of integer overflows and panics by proving that statements such as unreachable!() and panic!() are unreachable. Overflow checking can be disabled with a configuration flag, treating all integers as unbounded. In Prusti, the functional behaviour of a function can be specified by using annotations, among which are preconditions, postconditions, and loop invariants. The tool checks them, reporting error messages when the code does not adhere to the provided specification.
MIRAI #
Github: https://github.com/facebookexperimental/MIRAI
MIRAI is an abstract interpreter for the Rust compiler's mid-level intermediate representation (MIR). It is intended to become a widely used static analysis tool for Rust.